Welcome back to AA1.

If you're wondering why some of the seats are forbidden

there's something wrong apparently

with the air conditioning grills and they're worried that they might fall down.

So the university would rather not risk students and therefore they're forbidden.

So now you know.

Probably not because they took ample care.

I have my doubts that the grills will be able to be so accurate

but I'm just a computer

science professor and not a security expert

so why would I know?

Okay quiz is over

208 is nice

you did rather well

so that's fine.

Let me kind of go back to the unification algorithm we talked about last time.

We're doing something that may be new to you.

I'm saying algorithm

but I'm showing you an inference calculus.

And the idea there is that we're separating the logic from the control.

Syntactic means what can I do in principle and that's very well described by the inference

rules which are transformations on syntactic entities.

And this actually shows us the search space basically for solved forms and unsolvable

forms.

And now of course that's kind of the logic part

what can I do with this?

The control part is when do I do what?

Am I trying to do decomposition eagerly until nothing else can be decomposed or do I prefer

eliminations?

And that's a control question.

And the important fact here is we show a couple of things

correctness and completeness

or in other words we're not inventing any solutions or unifiers

we're not losing any

unifiers and it's confluent which means no matter what the sequences of the inference

rules are we always end up in the same result which also means there's that one most general

unifier.

So that makes the problem unitary which is again nice for all of the first order automated

theorem proving calculus.

This is a relatively good way of thinking about algorithms if we care about that they're

actually correct.

The thing here that's missing is termination

we talked in detail about termination because

it's another thing that becomes relatively easy if you write down your algorithm as a

set of transformations.

Okay?

You have to basically find out that there's something

the something turned out to be

relatively elaborate

that becomes smaller in every rule application.